proctype designatedDriver() {

byte K, pub, wench, inID;
byte num_of_wenches, num_of_sober_wenches;
bool cont;
mtype msg;

DRIVER_INIT:
SHUFFLE_LIST();

DRIVER_LOOP:

do

:: pubsVisited < N ->
	
	CHOOSE_TWO();
	/* ------ BARRIER 1 ------ */
	/* wait for everyone to be ready to vote for pubs */
	for(K : 0 .. (N-1)) {
		driverChannel?_;  
	}
	barrier5 = false;
	
	printf(" ------------------------- Round %d -----------------\n", pubsVisited);
	if
		:: debug -> printf(" -- Voting is between pub %d and pub %d \n", pubA, pubB);
		:: else -> skip
	fi;
	
	barrier1 = true;
	
	/* ----- BARRIER 2 ----- */
	/* wait for everyone to finish voting and check on winning condition */
	for(K : 0 .. (N-1)) {
		driverChannel?_;
	}
	barrier1 = false;
	CHECK_PUB_WIN(cont, pub);
	if
	:: cont -> pubsVisited++;
		if
			:: pub == pubA -> pubA = 255
			:: else -> pubB = 255
		fi;
	:: else -> goto GUARD_WIN_2PUBS
	fi;
	
	/* Pick up all the intoxicated delegates */
	for (K : 0 .. (N-1)) {
		currentPub[K] = pub;
	}
	printf ("Delegates arrived at pub %d\n", pub);
	barrier2 = true;
	
	for (K : 0 .. (N-1)) {
		driverChannel?_;
	}
	barrier2 = false;
	
	if
		:: (debug) -> printf("Wench vote between: \n");
			if
				:: wenchA.guard && wenchB.guard  -> printf ("Bodyguard %d and Bodyguard %d\n", wenchA.country, wenchB.country);
				:: wenchA.guard && !wenchB.guard -> printf ("Bodyguard %d and Delegate %d\n", wenchA.country, wenchB.country);
				:: !wenchA.guard && wenchB.guard -> printf ("Delegate %d and Bodyguard %d\n", wenchA.country, wenchB.country);
				:: else													 -> printf ("Delegate %d and Delegate %d\n", wenchA.country, wenchB.country);
			fi;
		:: else -> skip
	fi;

	barrier3 = true;
	
	num_of_sober_wenches = 0;
	num_of_wenches = 0;
	
	for (K : 0 .. (N-1)) {
		driverChannel?inID,msg;
		if
			:: msg == dwench && !intoxicated[inID] -> num_of_sober_wenches++;
				num_of_wenches++;
			:: else ->
				if
				:: msg == dwench || msg == gwench -> num_of_wenches++;
				:: else -> skip
				fi;
		fi;
		/* Ensure only one wench is actually elected */
		if
			:: num_of_wenches <= 1 -> drinkChannel[inID]!0,msg;
			:: else -> drinkChannel[inID]!0,ack;
		fi;
	}
	
	printf("Number of wenches elected: %d\n", num_of_wenches);
	
	barrier3 = false;
	if
		:: num_of_wenches == 0 -> goto GUARD_WIN_NOWENCHES
		:: num_of_sober_wenches > 1 ->  goto GUARD_WIN_2WENCHES
		:: else -> skip
	fi;
		
	barrier4 = true;
	
	for (K : 0 .. (N-1)) {
		driverChannel?_;
		
	}
	if
		:: guardIntoxicated -> goto GUARD_INTOXICATED_WIN
		:: else -> skip
	fi;
	
	barrier4 = false;
	barrier5 = true;

:: else -> 	goto DELEGATE_WIN 
	od;

DELEGATE_WIN:
atomic {
terminate = true;
printf("==============================\n");
printf("== PUB CRAWL WAS SUCCESSFUL ==\n");
printf("==============================\n");
}

goto END;
GUARD_WIN_2PUBS:
atomic {
terminate = true;
printf("==============================\n");
printf("==    DELEGATES GOT SPLIT   ==\n");
printf("==============================\n");
}
goto END;

GUARD_WIN_2WENCHES:
atomic {
terminate = true;
printf("==============================\n");
printf("==     TOO MANY WENCHES     ==\n");
printf("==============================\n");
}
goto END;

GUARD_WIN_NOWENCHES:
atomic {
terminate = true;
printf("==============================\n");
printf("==       NO BEER WENCH      ==\n");
printf("==============================\n");
}
goto END;

GUARD_INTOXICATED_WIN:
atomic {
terminate = true;
printf("==============================\n");
printf("==   GUARD WAS INTOXICATED  ==\n");
printf("==============================\n");
}

goto END;

END:
}